Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(app(if,true),xs),ys)  → xs
2:    app(app(app(if,false),xs),ys)  → ys
3:    app(app(sub,x),0)  → x
4:    app(app(sub,app(s,x)),app(s,y))  → app(app(sub,x),y)
5:    app(app(gtr,0),y)  → false
6:    app(app(gtr,app(s,x)),0)  → true
7:    app(app(gtr,app(s,x)),app(s,y))  → app(app(gtr,x),y)
8:    app(app(d,x),0)  → true
9:    app(app(d,app(s,x)),app(s,y))  → app(app(app(if,app(app(gtr,x),y)),false),app(app(d,app(s,x)),app(app(sub,y),x)))
10:    app(len,nil)  → 0
11:    app(len,app(app(cons,x),xs))  → app(s,app(len,xs))
12:    app(app(filter,p),nil)  → nil
13:    app(app(filter,p),app(app(cons,x),xs))  → app(app(app(if,app(p,x)),app(app(cons,x),app(app(filter,p),xs))),app(app(filter,p),xs))
There are 20 dependency pairs:
14:    APP(app(sub,app(s,x)),app(s,y))  → APP(app(sub,x),y)
15:    APP(app(sub,app(s,x)),app(s,y))  → APP(sub,x)
16:    APP(app(gtr,app(s,x)),app(s,y))  → APP(app(gtr,x),y)
17:    APP(app(gtr,app(s,x)),app(s,y))  → APP(gtr,x)
18:    APP(app(d,app(s,x)),app(s,y))  → APP(app(app(if,app(app(gtr,x),y)),false),app(app(d,app(s,x)),app(app(sub,y),x)))
19:    APP(app(d,app(s,x)),app(s,y))  → APP(app(if,app(app(gtr,x),y)),false)
20:    APP(app(d,app(s,x)),app(s,y))  → APP(if,app(app(gtr,x),y))
21:    APP(app(d,app(s,x)),app(s,y))  → APP(app(gtr,x),y)
22:    APP(app(d,app(s,x)),app(s,y))  → APP(gtr,x)
23:    APP(app(d,app(s,x)),app(s,y))  → APP(app(d,app(s,x)),app(app(sub,y),x))
24:    APP(app(d,app(s,x)),app(s,y))  → APP(app(sub,y),x)
25:    APP(app(d,app(s,x)),app(s,y))  → APP(sub,y)
26:    APP(len,app(app(cons,x),xs))  → APP(s,app(len,xs))
27:    APP(len,app(app(cons,x),xs))  → APP(len,xs)
28:    APP(app(filter,p),app(app(cons,x),xs))  → APP(app(app(if,app(p,x)),app(app(cons,x),app(app(filter,p),xs))),app(app(filter,p),xs))
29:    APP(app(filter,p),app(app(cons,x),xs))  → APP(app(if,app(p,x)),app(app(cons,x),app(app(filter,p),xs)))
30:    APP(app(filter,p),app(app(cons,x),xs))  → APP(if,app(p,x))
31:    APP(app(filter,p),app(app(cons,x),xs))  → APP(p,x)
32:    APP(app(filter,p),app(app(cons,x),xs))  → APP(app(cons,x),app(app(filter,p),xs))
33:    APP(app(filter,p),app(app(cons,x),xs))  → APP(app(filter,p),xs)
The approximated dependency graph contains 2 SCCs: {27} and {14,16,18,21,23,24,28,29,31,33}.
Tyrolean Termination Tool  (0.68 seconds)   ---  May 3, 2006